Search for: All records

We propose a concrete ("pointer as integer") memory semantics for C that supports verified compilation to a target environment having simple "public vs. private" data protection based on tagging or sandboxing (such as the WebAssembly virtual machine). Our semantics gives definition to a range of legacy programming idioms that cause undefined behavior in standard C, and are not covered by existing verified compilers, but that often work in practice. Compiler correctness in this context implies that target programs are secure against all control-flow attacks (although not against data-only attacks). To avoid tying our semantics too closely to particular compiler implementation choices, it is parameterized by a novel form of oracle that non-deterministically chooses the addresses of stack and heap allocations. As a proof-of-concept, we formalize a small RTL-like language and verify two-way refinement for a compiler from this language to a low-level machine and runtime system with hardware tagging. Our Coq formalization and proofs are provided as supplementary material. 

Abstract Microbial associations that result in phytoplankton mortality are important for carbon transport in the ocean. This includes parasitism, which in microbial food webs is dominated by the marine alveolate group, Syndiniales. Parasites are expected to contribute to carbon recycling via host lysis; however, knowledge on host dynamics and correlation to carbon export remain unclear and limit the inclusion of parasitism in biogeochemical models. We analyzed a 4-year 18S rRNA gene metabarcoding dataset (2016–19), performing network analysis for 12 discrete depths (1–1000 m) to determine Syndiniales–host associations in the seasonally oligotrophic Sargasso Sea. Analogous water column and sediment trap data were included to define environmental drivers of Syndiniales and their correlation with particulate carbon flux (150 m). Syndiniales accounted for 48–74% of network edges, most often associated with Dinophyceae and Arthropoda (mainly copepods) at the surface and Rhizaria (Polycystinea, Acantharea, and RAD-B) in the aphotic zone. Syndiniales were the only eukaryote group to be significantly (and negatively) correlated with particulate carbon flux, indicating their contribution to flux attenuation via remineralization. Examination of Syndiniales amplicons revealed a range of depth patterns, including specific ecological niches and vertical connection among a subset (19%) of the community, the latter implying sinking of parasites (infected hosts or spores) on particles. Our findings elevate the critical role of Syndiniales in marine microbial systems and reveal their potential use as biomarkers for carbon export. 

We introduce Tagged C, a novel C variant with built-in tag- based reference monitoring that can be enforced by hardware mecha- nisms such as the PIPE (Processor Interlocks for Policy Enforcement) processor extension. Tagged C expresses security policies at the level of C source code. It is designed to express a variety of dynamic security poli- cies, individually or in combination, and enforce them with compiler and hardware support. Tagged C supports multiple approaches to security and varying levels of strictness. We demonstrate this range by providing examples of memory safety, compartmentalization, and secure informa- tion flow policies. We also give a full formalized semantics and a reference interpreter for Tagged C. 

Microgrids must be able to restore voltage and frequency to their reference values during transient events; inverters are used as part of a microgrid's hierarchical control for maintaining power quality. Reviewed methods either do not allow for intuitive trade-off tuning between the objectives of synchronous state restoration, local reference tracking, and disturbance rejection, or do not consider all of these objectives. In this paper, we address all of these objectives for voltage restoration in droop-controlled inverter-based islanded micro-grids. By using distributed model predictive control (DMPC) in series with an unscented Kalman Filter (UKF), we design a secondary voltage controller to restore the voltage to the reference in finite time. The DMPC solves a reference tracking problem while rejecting reactive power disturbances in a noisy system. The method we present accounts for non-zero mean disturbances by design of a random-walk estimator. We validate the method's ability to restore the voltage in finite time via modeling a multi-node microgrid in Simulink.